package br.cin.ufpe.rabbit;

import gov.nasa.jpf.PropertyListenerAdapter;
import gov.nasa.jpf.jvm.ClassInfo;
import gov.nasa.jpf.jvm.ElementInfo;
import gov.nasa.jpf.jvm.FieldInfo;
import gov.nasa.jpf.jvm.Heap;
import gov.nasa.jpf.jvm.JVM;
import gov.nasa.jpf.jvm.MethodInfo;
import gov.nasa.jpf.jvm.StackFrame;
import gov.nasa.jpf.jvm.ThreadInfo;
import gov.nasa.jpf.jvm.ThreadList;
import gov.nasa.jpf.jvm.bytecode.FieldInstruction;
import gov.nasa.jpf.jvm.bytecode.GETFIELD;
import gov.nasa.jpf.jvm.bytecode.GETSTATIC;
import gov.nasa.jpf.jvm.bytecode.INVOKESPECIAL;
import gov.nasa.jpf.jvm.bytecode.Instruction;
import gov.nasa.jpf.jvm.bytecode.NEW;
import gov.nasa.jpf.jvm.bytecode.PUTFIELD;
import gov.nasa.jpf.jvm.bytecode.PUTSTATIC;
import gov.nasa.jpf.search.Search;
import gov.nasa.jpf.util.HashData;
import gov.nasa.jpf.util.Pair;

import java.util.ArrayList;
import java.util.Calendar;
import java.util.Comparator;
import java.util.Date;
import java.util.HashMap;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Set;
import java.util.TreeMap;
import java.util.TreeSet;

import sun.print.PeekGraphics;

import br.cin.ufpe.rabbit.ObjectIdListener.Status;
import br.cin.ufpe.rabbit.PotentialRaceInfo.MemoryAccess;
import br.cin.ufpe.rabbit.RabbitConfig.Distance;
import br.cin.ufpe.rabbit.RabbitConfig.ExecutionMode;
import br.cin.ufpe.rabbit.RabbitConfig.Report;

public class RabbitListener extends PropertyListenerAdapter {

	static boolean useRabbitHash = StackFrame.useRabbitHash;
	//maps JPF ids in Rabbit Ids
	static Map<Integer,Integer> objIdLogs = new HashMap<Integer,Integer>();

	public void objectCreated(JVM vm) {
	}

	public void choiceGeneratorSet(JVM vm) {
		// System.out.println(vm.getRunnableThreadCount());
	}

	public void threadStarted(JVM vm) {
		// System.out.println("thread STarted");

	}

	public void threadScheduled(JVM vm) {
		// System.out.println("thread Scheduled");
	}

	/**
	 * field rw-sets maps JPF object ids (integers) to a map of field info to
	 * read-write sets
	 */
	private Map<Integer, Map<FieldInfo, Map<ThreadInfo, Map<Instruction, List<MemoryAccess>>>>> rwsets = new TreeMap<Integer, Map<FieldInfo, Map<ThreadInfo, Map<Instruction, List<MemoryAccess>>>>>();

	public static Map<Integer, PotentialRaceInfo> interesting = new TreeMap<Integer, PotentialRaceInfo>();

	/** uses the same package as main function */
	private String PACK_TO_ANALYZE;

	private boolean potencialBugfound = false;

	static int count = 0;

	/**
	 * about to execution one instruction
	 */
	public void executeInstruction(JVM vm) {

		/*************************************************
		 * TODO: consider array fields if necessary, later
		 *************************************************/
		Instruction insn = vm.getLastInstruction();

		if (insn == null) {
			return;
		}

		// agressive otimization
		if (vm.getThreadList().getLiveThreadCount() < 2) {
			return;
		}

		if (insn instanceof FieldInstruction
				&& !ShouldAnalize(((FieldInstruction) insn).getFieldInfo(),
						insn)) {
			return;
		}

		if (insn.getByteCode() == RabbitConfig.PUTFIELD_opcode) {

			PUTFIELD pf = (PUTFIELD) insn;
			FieldInfo fi = pf.getFieldInfo();
			ThreadInfo ti = vm.getCurrentThread();

			int storageSize = fi.getStorageSize();
			int objRef = ti.peek((storageSize == 1) ? 1 : 2);
			//if(objRef == 343){
	
			//}			
			if (useRabbitHash) {
				int rabbitID = vm.getHeap().get(objRef).getObjectIdHash();
				String stack = vm.getCurrentThread().getStack().toString();
				vm.storeTrace("/home/jpso/tmp/logs/objIds/"+objRef, "jpf id "+objRef+ " rabbit id " + rabbitID + "\n stack: "+stack , true);
				objIdLogs.put(objRef, rabbitID);
				objRef = vm.getHeap().get(objRef).getObjectIdHash();
			}else{
				int rabbitID = vm.getHeap().get(objRef).getObjectIdHash();
				String stack = vm.getCurrentThread().getStack().toString();
				vm.storeTrace("/home/jpso/tmp/logs/objIds/"+objRef, "jpf id "+objRef+ " rabbit id " + rabbitID + "\n stack: "+stack , true);
				objIdLogs.put(objRef, rabbitID);
			}
			update(objRef, fi, insn, ti);
		} else if (insn.getByteCode() == RabbitConfig.GETFIELD_opcode) {

			GETFIELD gf = (GETFIELD) insn;
			ThreadInfo ti = vm.getCurrentThread();
			FieldInfo fi = gf.getFieldInfo();

			if (ti.getTopFrame().getTopPos() != -1) {
				int objRef = ti.peek();
				if (useRabbitHash) {
					int rabbitID = vm.getHeap().get(objRef).getObjectIdHash();
					objIdLogs.put(objRef, rabbitID);
					objRef = vm.getHeap().get(objRef).getObjectIdHash();
				}else{
					int rabbitID = vm.getHeap().get(objRef).getObjectIdHash();
					objIdLogs.put(objRef, rabbitID);
				}
				update(objRef, fi, insn, ti);
			}
		} else if (insn.getByteCode() == RabbitConfig.PUTSTATIC_opcode) {

			PUTSTATIC ps = (PUTSTATIC) insn;
			FieldInfo fi = ps.getFieldInfo();
			ThreadInfo ti = vm.getCurrentThread();
			
			int objRef;
			if (useRabbitHash) {
				objRef = (ps.getClassInfo().getName() + "." + ps.getFieldInfo()
						.getName()).hashCode();
			}else{
				int rabbitID = (ps.getClassInfo().getName() + "." + ps.getFieldInfo()
						.getName()).hashCode();
				//int storageSize = fi.getStorageSize();
				objRef = rabbitID;//ti.peek((storageSize == 1) ? 1 : 2);
			//	objIdLogs.put(objRef, rabbitID);
			}
			
			// int storageSize = fi.getStorageSize();
			// int objRef = ti.peek((storageSize == 1) ? 1 : 2);
			update(objRef, fi, insn, ti);
		} else if (insn.getByteCode() == RabbitConfig.GETSTATIC_opcode) {

			GETSTATIC gs = (GETSTATIC) insn;
			ThreadInfo ti = vm.getCurrentThread();
			FieldInfo fi = gs.getFieldInfo();

			int objRef;
			if (useRabbitHash) {
				objRef = (gs.getClassInfo().getName() + "." + gs.getFieldInfo()
						.getName()).hashCode();
			}else{
				int rabbitID = (gs.getClassInfo().getName() + "." + gs.getFieldInfo()
						.getName()).hashCode();
			//	int storageSize = fi.getStorageSize();
				objRef = rabbitID;//ti.peek((storageSize == 1) ? 1 : 2);
				//objIdLogs.put(objRef, rabbitID);
			}

			update(objRef, fi, insn, ti);
			// int storageSize = fi.getStorageSize();
			// int objRef = ti.peek((storageSize == 1) ? 1 : 2);
		}
		runtimeCheckRace(vm.getCurrentThread());
		
	}

	/**
	 * auxiliary method to update rwset data
	 * 
	 * @param objRef
	 * @param fi
	 * @param insn
	 * @param ti
	 */
	private void update(int objRef, FieldInfo fi, Instruction insn,
			ThreadInfo ti) {

		if (!ShouldAnalize(fi, insn)) {
			return;
		}

		// TODO: optimize this!
		Map<FieldInfo, Map<ThreadInfo, Map<Instruction, List<MemoryAccess>>>> map1 = rwsets
				.get(objRef);
		if (map1 == null) {
			if (RabbitConfig.SHOW_PROGRESS)
				RabbitConfig.testReport(null, Report.O, countStateAdvanced,
						false);
			map1 = new TreeMap<FieldInfo, Map<ThreadInfo, Map<Instruction, List<MemoryAccess>>>>(
					fiComparator);
			rwsets.put(objRef, map1);
		}
		Map<ThreadInfo, Map<Instruction, List<MemoryAccess>>> map2 = map1
				.get(fi);
		if (map2 == null) {
			// if (Config.SHOW_PROGRESS) signal('B');
			if (RabbitConfig.SHOW_PROGRESS)
				RabbitConfig.testReport(null, Report.F, countStateAdvanced,
						false);
			map2 = new TreeMap<ThreadInfo, Map<Instruction, List<MemoryAccess>>>(
					tiComparator);
			map1.put(fi, map2);
		}

		Map<Instruction, List<MemoryAccess>> map3 = map2.get(ti);
		if (map3 == null) {
			// if (Config.SHOW_PROGRESS) signal('C');
			if (RabbitConfig.SHOW_PROGRESS)
				RabbitConfig.testReport(null, Report.T, countStateAdvanced,
						false);
			map3 = new TreeMap<Instruction, List<MemoryAccess>>(insnComparator);
			map2.put(ti, map3);
		}
		List<MemoryAccess> mAccess = map3.get(insn);
		if (mAccess == null) {
			mAccess = new ArrayList<MemoryAccess>();
			map3.put(insn, mAccess);
		}

		// initialize set of element info
		List<ElementInfo> li = ti.getLockedObjects();
		Set<ElementInfo> sei = new TreeSet<ElementInfo>(RabbitConfig.comp);
		sei.addAll(li);

		// check if there is an equal set
		boolean hasLockSet = false, hasThreadList = false;

		List<ThreadInfo> tempTiList = new ArrayList<ThreadInfo>();
		// check if is the best choice getLiveThreads or getThreadList
		for (ThreadInfo threadInfo : ti.getVM().getLiveThreads()) {
			tempTiList.add(threadInfo);
		}

		for (MemoryAccess tmp : mAccess) {
			if (tmp.lockSet.equals(sei)) {
				hasLockSet = true;
			}
			if (tmp.runningThreads.containsAll(tempTiList)) {
				hasThreadList = true;
			}
		}
		if (hasLockSet) {
			return; // interesting itens already had been computed
		}
		// optimize to avoid repeated itens
		MemoryAccess newMAccess = new MemoryAccess(sei, tempTiList);
		mAccess.add(newMAccess);
		/**
		 * check whether or not this entry should be added to the interesting
		 * set!
		 * 
		 * if there is another thread whose intersection of access monitor set
		 * is empty.
		 */
		// if (interesting.containsKey(objRef)) {
		// // return;
		// }

		boolean hasWrite = isWrite(insn.getByteCode());
		boolean inconsistentLockSets = false;
		boolean targetIsEmptyRead = !isWrite(insn.getByteCode())
				&& li.isEmpty();
		a: for (Map.Entry<ThreadInfo, Map<Instruction, List<MemoryAccess>>> entry : map2
				.entrySet()) {
			for (Map.Entry<Instruction, List<MemoryAccess>> entry2 : entry
					.getValue().entrySet()) {
				boolean isWrite = isWrite(entry2.getKey().getByteCode());
				boolean isRead = !isWrite;
				hasWrite = hasWrite || isWrite;
				for (MemoryAccess monitorSet : entry2.getValue()) {
					/**
					 * CASE 1: target access is a read with empty lock set.
					 * subject access is a write with a non-empty write.
					 * accesses are in different threads
					 */
					if (targetIsEmptyRead && isWrite
							&& !monitorSet.lockSet.isEmpty()) {

						PotentialRaceInfo raceInfo = new PotentialRaceInfo(
								objRef, fi, map2);
						interesting.put(objRef, raceInfo);
						if (RabbitConfig.SHOW_PROGRESS)
							RabbitConfig.testReport(null, Report.STAR,
									countStateAdvanced, false);
						break a;
					}
					/**
					 * CASE 2: inconsistent locking discipline
					 */
					if (isRead)
						continue;
					@SuppressWarnings("unchecked")
					Set<ElementInfo> clone = ((Set<ElementInfo>) ((TreeSet<ElementInfo>) monitorSet.lockSet)
							.clone());
					clone.retainAll(li);
					inconsistentLockSets = inconsistentLockSets
							|| clone.isEmpty();
					if (!targetIsEmptyRead && hasWrite /*
														 * &&
														 * inconsistentLockSets
														 */) {
						/**************************************************
						 * note that object map2 can is shared with the map
						 * object stored in variable rwsets and potentially
						 * shared with other PotentialRaceInfo objects
						 **************************************************/
						PotentialRaceInfo raceInfo = new PotentialRaceInfo(
								objRef, fi, map2);
						interesting.put(objRef, raceInfo);
						if (RabbitConfig.SHOW_PROGRESS)
							RabbitConfig.testReport(null, Report.STAR,
									countStateAdvanced, false);
						break a;
					}
				}
			}
		}

		// runtimeCheckRace(ti);

	}

	int races = 0;

	private void runtimeCheckRace(ThreadInfo ti) {
		if (RabbitConfig.RUNTIME_CHECK_RACES) {
			// System.out.println("checking Runtime Races");
			List<Pair<FieldInstruction, Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>>>> result = new ArrayList<Pair<FieldInstruction, Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>>>>();
			for (PotentialRaceInfo pri : interesting.values()) {
				pri.filterPotentialRaceList(result);
			}

			removeDuplicatedReports(result);

			if (!result.isEmpty() && result.size() > races) {
				races = result.size();
				// search.
				// potencialBugfound = true;
				Date startDate = ti.getVM().getJPF().getReporter()
						.getStartDate();
				Date CurrentDate = Calendar.getInstance().getTime();
				long diffTime = CurrentDate.getTime() - startDate.getTime();
				System.out.println("========== \ntotal:" + races + " \n "
						+ "diffTime : " + diffTime);
				searchFinished(ti.getVM().getJPF().getSearch());
				// ti.get
				// ti.getVM().getJPF().exit();
				// throw new RuntimeException("Found a Race. Running Time is "+
				// diffTime);

			}

		}
	}

	private boolean ShouldAnalize(FieldInfo fi, Instruction insn) {
		boolean returnValue = true;
		ClassInfo cInfo = fi.getClassInfo();
		if (!cInfo.getPackageName().startsWith(PACK_TO_ANALYZE)) {
			return false;
		}
		MethodInfo mInfo = insn.getMethodInfo();
		if (RabbitConfig.IGNORE_CLINIT && mInfo.isClinit()) {
			return false;
		}
		if (RabbitConfig.IGNORE_INIT && mInfo.isCtor()) {
			return false;
		}
		String name = mInfo.getName();
		if (RabbitConfig.IGNORE_RUN && name.startsWith("run")) {
			return false;
		}
		if (RabbitConfig.IGNORE_MAIN && name.startsWith("main")) {
			return false;
		}
		return returnValue;
	}

	public static boolean isWrite(int byteCode) {
		return byteCode == RabbitConfig.PUTFIELD_opcode
				|| byteCode == RabbitConfig.PUTSTATIC_opcode;
	}

	@Override
	public void searchStarted(Search search) {
		super.searchStarted(search);
		String s = search.getVM().getMainClassInfo().getPackageName();
		int dot = s.indexOf(".");
		if (dot == -1 /* dot not found */) {
			PACK_TO_ANALYZE = s;
		} else {
			PACK_TO_ANALYZE = s.substring(0, dot);
		}

		// Configure Rabbit
		RabbitConfig.TIME_UNTIL_STOP = search.getConfig().getInt("stop_time",
				-1);

		RabbitConfig.IGNORE_INIT = JVM.getVM().getConfig()
				.getBoolean("IGNORE.INIT", false);
		RabbitConfig.IGNORE_RUN = JVM.getVM().getConfig()
				.getBoolean("IGNORE.RUN", false);
		RabbitConfig.IGNORE_CLINIT = JVM.getVM().getConfig()
				.getBoolean("IGNORE.CLINIT", true);
		RabbitConfig.IGNORE_MAIN = JVM.getVM().getConfig()
				.getBoolean("IGNORE.MAIN", false);
		RabbitConfig.SHOW_PROGRESS = JVM.getVM().getConfig()
				.getBoolean("SHOW.PROGRESS", false);
		RabbitConfig.SHOW_STATE_GENERATION = JVM.getVM().getConfig()
				.getBoolean("SHOW.STATE.GENERATION", false);
		RabbitConfig.SHOW_DETAILED_STATE_GENERATION = JVM.getVM().getConfig()
				.getBoolean("SHOW.DETAILED.STATE.GENERATION", false);

		RabbitConfig.RUNTIME_CHECK_RACES = JVM.getVM().getConfig()
				.getBoolean("Rabbit.Runtime.checkRace", false);

		RabbitConfig.distance = Distance.valueOf(JVM.getVM().getConfig()
				.getString("DISTANCE", RabbitConfig.distance.toString()));

	}

	@Override
	public void searchFinished(Search search) {
		// super.searchFinished(search);
		switch (RabbitConfig.opt) {
		case PRINT_RWSETS:
			dump(search);
			break;
		case PRINT_INTERESTING:
		// prints the obj ids and Rabbit ids
		//	System.out.println("=========object ids============");
		//	for (Entry<Integer,Integer> IdLogs : objIdLogs.entrySet()) {
		//		System.out.printf("JPF id: %s => rabbit id: %s \n", IdLogs.getKey(), IdLogs.getValue() );
		//	}
			
			System.out.println("========potential races========");
			// interesting.remove(-1);
			for (PotentialRaceInfo pri : interesting.values()) {
				pri.Analize(search);
				String output = pri.dump(search, false);
				if (!output.equals("")) {
					System.out.println(output);
				}
			}
			int k = -1;
			System.out.println("======== sumary ========");
			List<Pair<FieldInstruction, Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>>>> result = new ArrayList<Pair<FieldInstruction, Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>>>>();
			for (PotentialRaceInfo pri : interesting.values()) {
				pri.filterPotentialRaceList(result);
			}

			removeDuplicatedReports(result); // optimization II

			int i = 0;
			for (Pair<FieldInstruction, Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>>> potRaces : result) {

				String m1 = potRaces._2._1._2.getClassName() + "."
						+ potRaces._2._1._2.getName();
				String m2 = potRaces._2._2._2.getClassName() + "."
						+ potRaces._2._2._2.getName();

				System.out
						.printf("%s >Potential race for field %s \nwrite: [%s] %s\nread: [%s] %s\n<\n",
								++i, potRaces._1.getFieldInfo().getFullName(),
								potRaces._2._1._1.getName(), m1,
								potRaces._2._2._1.getName(), m2);

			}
			break;
		// System.out.println("========detailed========");
		// for (PotentialRaceInfo pri : interesting.values()) {
		// System.out.println(pri.toString(search));
		// }
		// System.out.println("========compacted=======");
		// List<Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo,
		// MethodInfo>>> result = new ArrayList<Pair<Pair<ThreadInfo,
		// MethodInfo>, Pair<ThreadInfo, MethodInfo>>>();
		// for (PotentialRaceInfo pri : interesting.values()) {
		// pri.updatePotentialRacesList(result);
		// }
		// int i =0;
		// for (Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>>
		// potRaces : result) {
		// System.out.printf(">Potential race for field %s \nwrite: %s, %s\nread: %s, %s\n<\n",i,
		// potRaces._1._1,
		// potRaces._1._2, potRaces._2._1, potRaces._2._2);
		// i++;
		// }
		// break;
		case PRINT_ALL:
			dump(search);
			System.out.println("========================");
			for (PotentialRaceInfo pri : interesting.values()) {
				System.out.println(pri.toString(search));
			}
			break;
		default:
			break;
		}
	}

	private void removeDuplicatedReports(
			List<Pair<FieldInstruction, Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>>>> potRaces) {
		if (potRaces.size() == 0) {
			return;
		}

		for (int i = 0; i < potRaces.size(); i++) {
			Pair<FieldInstruction, Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>>> item = potRaces
					.get(i);

			// loops backward looking for equals reports
			for (int j = potRaces.size() - 1; j > i; j--) {
				Pair<FieldInstruction, Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>>> item2 = potRaces
						.get(j);
				if (item._1
						.getFieldInfo()
						.getFullName()
						.equals(potRaces.get(j)._1.getFieldInfo().getFullName())
						&& item._2._1._2.getName().equals(
								item2._2._1._2.getName())
						&& item._2._2._2.getName().equals(
								item2._2._2._2.getName())) {
					potRaces.remove(j);
				}
			}
		}
	}

	private void dump(Search search) {
		Set<ElementInfo> monitors = new TreeSet<ElementInfo>(RabbitConfig.comp);
		Heap heap = search.getVM().getSystemState().getHeap();
		for (Map.Entry<Integer, Map<FieldInfo, Map<ThreadInfo, Map<Instruction, List<MemoryAccess>>>>> entry : rwsets
				.entrySet()) {
			int id = entry.getKey();
			String msg = null;
			switch (id) {
			case RabbitConfig.MOCK_CLASS_ID:
				msg = "static field";
				break;
			case -1:
				msg = "null reference";
				break;
			default:
				try {
					msg = heap.get(id).getClassInfo().getName();
				} catch (NullPointerException _) {
				}
				break;
			}
			if (msg == null) {
				System.out.printf("object id: %d (%s)\n", id,
						"garbage collected");
				// continue;
			}
			System.out.printf("object id: %d (%s)\n", id, msg);

			for (Map.Entry<FieldInfo, Map<ThreadInfo, Map<Instruction, List<MemoryAccess>>>> entry2 : entry
					.getValue().entrySet()) {
				System.out.printf("  field: %s\n", entry2.getKey());
				Map<ThreadInfo, Map<Instruction, List<MemoryAccess>>> tmap = entry2
						.getValue();
				if (tmap.size() < 2) { /* SAFE */
					continue;
				}
				for (Map.Entry<ThreadInfo, Map<Instruction, List<MemoryAccess>>> entry3 : tmap
						.entrySet()) {
					ThreadInfo ti = entry3.getKey();
					System.out.printf("    thread id: %s (%s)\n", ti.getId(),
							ti.getName());
					for (Map.Entry<Instruction, List<MemoryAccess>> entry4 : entry3
							.getValue().entrySet()) {
						Instruction insn = entry4.getKey();
						int opcode = insn.getByteCode();
						String msg2 = (opcode == RabbitConfig.PUTFIELD_opcode) ? "WRITE"
								: (opcode == RabbitConfig.PUTSTATIC_opcode) ? "WRITE"
										: "READ";
						System.out.printf("      instruction: %s %s",
								insn.getSourceLocation(), msg2);
						System.out.print(" [");
						List<MemoryAccess> set = entry4.getValue();
						for (MemoryAccess ma : set) {
							monitors.addAll(ma.lockSet);
							int i = 0, size = ma.lockSet.size();
							System.out.print("(");
							for (ElementInfo ei : ma.lockSet) {
								i++;
								System.out.print(ei.getIndex());
								if (i < size) {
									System.out.print(", ");
								}
							}
							System.out.print(")");
						}
						System.out.println("] ");
					}
				}
			}
		}
		System.out.println("============================");
		for (ElementInfo ei : monitors) {
			System.out.printf("monitor id %d %s\n", ei.getIndex(), ei
					.getClassInfo().getName());
		}
	}

	public static Comparator<FieldInfo> fiComparator = new Comparator<FieldInfo>() {
		@Override
		public int compare(FieldInfo arg0, FieldInfo arg1) {
			return ((Integer) arg0.hashCode()).compareTo(arg1.hashCode());
		}
	};

	static Comparator<ThreadInfo> tiComparator = new Comparator<ThreadInfo>() {
		@Override
		public int compare(ThreadInfo arg0, ThreadInfo arg1) {
			return arg0.compareTo(arg1);
		}
	};

	static Comparator<Instruction> insnComparator = new Comparator<Instruction>() {
		@Override
		public int compare(Instruction arg0, Instruction arg1) {
			return ((Integer) arg0.hashCode()).compareTo(arg1.hashCode());
		}
	};

	int countStateAdvanced = 0;

	@Override
	public void stateAdvanced(Search search) {
		// runtimeCheckRace(search.getVM().getLastThreadInfo());
		checkTime(search, search.getVM());
		if (RabbitConfig.SHOW_PROGRESS) {
			br.cin.ufpe.rabbit.RabbitConfig.testReport(search,
					RabbitConfig.report, countStateAdvanced, false);
		}

	}

	private String errorMessage;

	public void checkTime(Search search, JVM vm) {
		Date startDate = vm.getJPF().getReporter().getStartDate();
		Date CurrentDate = Calendar.getInstance().getTime();

		long diffTime = CurrentDate.getTime() - startDate.getTime();

		if (RabbitConfig.TIME_UNTIL_STOP > 0
				&& diffTime > RabbitConfig.TIME_UNTIL_STOP) {
			errorMessage = "search time finished - "
					+ RabbitConfig.TIME_UNTIL_STOP + "ms";

			// System.err.println("FINISHED!!!!");
			// search.error(this);
			search.terminate();
		}
	}

	@Override
	public boolean check(Search search, JVM vm) {

		if (potencialBugfound) {
			errorMessage = "potencial bug found";
			return false;
		}

		return true;
	}

	@Override
	public String getErrorMessage() {
		return errorMessage;
	}

	@Override
	public String getExplanation() {
		// TODO Auto-generated method stub
		return null;
	}

	@Override
	public void reset() {
		// TODO Auto-generated method stub

	}

	public static List<Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>>> potencialRaceConflicts = null;;

	/**
	 * extract all potential race Info, just if PotencialRaceConflicts is empty
	 * 
	 * @return
	 */
	public static List<Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>>> extractPotencialConficts() {
		potencialRaceConflicts = new ArrayList<Pair<Pair<ThreadInfo, MethodInfo>, Pair<ThreadInfo, MethodInfo>>>();

		for (PotentialRaceInfo pri : RabbitListener.interesting.values()) {
			pri.updatePotentialRacesList(potencialRaceConflicts);
		}
		return potencialRaceConflicts;
	}

}